test(fields): extend Mersenne31 regression coverage - #260

CompPoly/Fields/Mersenne.lean (3)

• abbrev Field
• def fieldSize : Nat
• theorem is_prime : Nat.Prime fieldSize

CompPoly/Fields/Mersenne31/Basic.lean (3)

• abbrev Field
• def fieldSize : Nat
• theorem is_prime : Nat.Prime fieldSize

CompPoly/Fields/Mersenne31/Fast.lean (105)

• abbrev Field : Type
• def add (x y : Field) : Field
• def div (x y : Field) : Field
• def inv (x : Field) : Field
• def modulus : UInt32
• def mul (x y : Field) : Field
• def neg (x : Field) : Field
• def ofField (x : Mersenne31.Basic.Field) : Field
• def ofInt (z : Int) : Field
• def ofNat (n : Nat) : Field
• def ofUInt32 (x : UInt32) : Field
• def pow (x : Field) (n : Nat) : Field
• def raw (x : Field) : UInt32
• def ringEquiv : Field ≃+* Mersenne31.Basic.Field where
• def square (x : Field) : Field
• def sub (x y : Field) : Field
• def toField (x : Field) : Mersenne31.Basic.Field
• def toNat (x : Field) : Nat
• instance instAddField : Add Field where
• instance instDivField : Div Field where
• instance instIntCastField : IntCast Field where
• instance instIntSMulField : SMul Int Field where
• instance instInvField : Inv Field where
• instance instMulField : Mul Field where
• instance instNNRatCastField : NNRatCast Field where
• instance instNNRatSMulField : SMul ℚ≥0 Field where
• instance instNatCastField : NatCast Field where
• instance instNatSMulField : SMul Nat Field where
• instance instNegField : Neg Field where
• instance instOneField : One Field where
• instance instPowFieldInt : Pow Field Int where
• instance instPowFieldNat : Pow Field Nat where
• instance instRatCastField : RatCast Field where
• instance instRatSMulField : SMul ℚ Field where
• instance instSubField : Sub Field where
• instance instZeroField : Zero Field where
• private def invExponent : Nat
• private def modulus64 : UInt64
• private def ofCanonicalNat (n : Nat) (h : n < Mersenne31.Basic.fieldSize) : Field
• private def one : Field
• private def reduceUInt32Lt2Modulus (x : UInt32)
• private def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32
• private def reduceUInt64 (x : UInt64)
• private def reduceUInt64Raw (x : UInt64) : UInt32
• private def shift4Mul (acc digit : Field) : Field
• private def zero : Field
• private theorem fieldSize_add_fieldSize_lt_uint32Size :
• private theorem fieldSize_lt_uint32Size : Mersenne31.Basic.fieldSize < UInt32.size
• private theorem fieldSize_mul_fieldSize_lt_two64 :
• private theorem fieldSize_pos : 0 < Mersenne31.Basic.fieldSize
• private theorem modulus64_toNat : modulus64.toNat = Mersenne31.Basic.fieldSize
• private theorem mul_assoc_field (x y z : Field) : (x * y) * z = x * (y * z)
• private theorem pow_succ (x : Field) (n : Nat) : pow x (n + 1) = pow x n * x
• private theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32)
• private theorem reduceUInt32Lt2Modulus_cast (x : UInt32)
• private theorem reduceUInt64Raw_lt (x : UInt64)
• private theorem reduceUInt64Raw_split_toNat (x : UInt64)
• private theorem reduceUInt64_cast (x : UInt64)
• private theorem toField_injective : Function.Injective toField
• private theorem toField_inv_pow (x : Field) :
• private theorem toField_mul_pow (base x y : Field) (m n : Nat)
• private theorem toField_ofCanonicalNat (n : Nat) (h : n < Mersenne31.Basic.fieldSize) :
• private theorem toField_reduceUInt64 (x : UInt64)
• private theorem toField_shift4Mul (acc digit : Field) :
• private theorem toField_shift4Mul_pow (base acc digit : Field) (e d : Nat)
• private theorem toNat_ofCanonicalNat (n : Nat) (h : n < Mersenne31.Basic.fieldSize) :
• theorem modulus_toNat : modulus.toNat = Mersenne31.Basic.fieldSize
• theorem ofField_toField (x : Field) :
• theorem raw_eq_val (x : Field) : raw x = x.val
• theorem raw_mk (x : UInt32) (h : x.toNat < Mersenne31.Basic.fieldSize) :
• theorem raw_one : raw (1 : Field) = 1
• theorem raw_zero : raw (0 : Field) = 0
• theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x
• theorem ringEquiv_symm_apply (x : Mersenne31.Basic.Field) : ringEquiv.symm x = ofField x
• theorem toField_add (x y : Field) :
• theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y
• theorem toField_intCast (n : Int) :
• theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹
• theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y
• theorem toField_natCast (n : Nat) :
• theorem toField_neg (x : Field) : toField (-x) = -toField x
• theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x
• theorem toField_nnratCast (q : ℚ≥0) :
• theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n
• theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x
• theorem toField_ofField (x : Mersenne31.Basic.Field) :
• theorem toField_ofInt (z : Int) :
• theorem toField_ofNat (n : Nat) :
• theorem toField_ofUInt32 (x : UInt32) :
• theorem toField_one : toField (1 : Field) = 1
• theorem toField_pow (x : Field) (n : Nat) : toField (pow x n) = toField x ^ n
• theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x
• theorem toField_ratCast (q : ℚ) :
• theorem toField_square (x : Field) : toField (square x) = toField x * toField x
• theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y
• theorem toField_zero : toField (0 : Field) = 0
• theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n
• theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x
• theorem toNat_eq_val_toNat (x : Field) : toNat x = x.val.toNat
• theorem toNat_mk (x : UInt32) (h : x.toNat < Mersenne31.Basic.fieldSize) :
• theorem toNat_ofField (x : Mersenne31.Basic.Field) : toNat (ofField x) = x.val
• theorem toNat_ofNat (n : Nat) :
• theorem toNat_ofUInt32 (x : UInt32) :
• theorem toNat_one : toNat (1 : Field) = 1
• theorem toNat_zero : toNat (0 : Field) = 0

tests/CompPolyTests/Fields/Mersenne31.lean (6)

• example : (2 : Basic.Field) ≠ 0
• example : Fact (Nat.Prime Basic.fieldSize)
• example : NonBinaryField Basic.Field
• example : NonBinaryField Field
• example : _root_.Field Basic.Field
• example : _root_.Field Field

The diff restructures the Mersenne field implementation, replacing the single-file Mersenne.lean with a Mersenne31/ directory containing Basic.lean, Fast.lean, and a facade. The changes largely follow the project's naming and file conventions, but multiple violations of the style guide are present, particularly regarding documentation and line length.

• CompPoly.lean: The import of CompPoly.Fields.Mersenne is replaced by three imports: CompPoly.Fields.Mersenne31, CompPoly.Fields.Mersenne31.Basic, and CompPoly.Fields.Mersenne31.Fast. This reflects a reorganization or renaming of the Mersenne field module, splitting it into a base module and submodules for basic and fast operations.
• CompPoly/Fields/Mersenne31.lean: This new file CompPoly/Fields/Mersenne31.lean serves as a facade module for the Mersenne31 field ($2^{31} - 1$). It imports and re-exports the canonical ZMod model from CompPoly.Fields.Mersenne31.Basic and the native-word implementation from CompPoly.Fields.Mersenne31.Fast, providing a single import point for users. No definitions or theorems are declared in this file; it only re-exports existing content.
• CompPoly/Fields/Mersenne31/Basic.lean: Added a new file CompPoly/Fields/Mersenne31/Basic.lean that defines the Mersenne31 prime field 2^{31}-1. It introduces fieldSize as 2^31 - 1, Field as ZMod fieldSize, and proves is_prime via the pratt tactic. It then registers a Fact (Nat.Prime fieldSize) instance, a Field instance for Field, and a NonBinaryField instance with char_neq_2 proved by decide. No sorry or admit are present.
• CompPoly/Fields/Mersenne31/Fast.lean: This 994-line file adds a new Fast submodule in CompPoly/Fields/Mersenne31/ that defines Fast.Field, a UInt32-backed subtype of canonical representatives below 2^31 - 1. It provides the core arithmetic operations (add, sub, neg, mul, square, pow, inv, div), supporting casts (ofNat, toNat, ofField, toField, ofUInt32, ofInt), and corresponding typeclass instances (Zero, One, Add, Sub, Neg, Mul, Inv, Div, NatCast, IntCast, Pow, SMul for ℕ, ℤ, ℚ≥0, ℚ), plus a ringEquiv to the canonical Mersenne31.Basic.Field. A Field instance is transferred via toField_injective.field, and a NonBinaryField instance is provided. Key correctness lemmas (toField_add, toField_mul, toField_inv) prove that each fast operation agrees with the corresponding operation in the canonical field, and the inversion chain computes x^(p-2) using a fixed addition chain. The file is complete; it contains no sorry or admit.
• tests/CompPolyTests.lean: Added an import of CompPolyTests.Fields.Mersenne31, making the Mersenne31 field module available in the test file. This ensures that any tests or definitions related to the Mersenne31 field are included and can be exercised as part of the test suite.
• tests/CompPolyTests/Fields/Mersenne31.lean: This new test file adds regression checks for the Mersenne31 field surfaces (Basic.Field and Fast.Field). It verifies that Basic.Field is a field and a NonBinaryField (by checking char_neq_2), and that Fast.Field is a field and a NonBinaryField. The file then provides a comprehensive suite of #guard statements for the fast surface, testing raw, toNat, toField, and ringEquiv operations, including addition, subtraction, negation, multiplication, squaring, exponentiation (both Nat and Int), inverse, and division, with explicit edge cases for zero and the modulus boundary.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): CompPoly/Fields/Mersenne.lean

tests/CompPolyTests/Fields/Mersenne31/Instances.lean (6)

• example : (2 : Field) ≠ 0
• example : Fact (Nat.Prime fieldSize)
• example : NonBinaryField Field
• example : NonBinaryField Field
• example : _root_.Field Field
• example : _root_.Field Field

• The new file tests/CompPolyTests/Fields/Mersenne31/Instances.lean has an incomplete module declaration: the line module is missing the module name (should be module CompPolyTests.Fields.Mersenne31.Instances).
• The same file uses public section which is invalid syntax; section does not accept a visibility modifier in Lean. This will cause a compilation error.
• The public keyword on import is allowed but unusual for test files; consider omitting it unless reexport is intentional.

• tests/CompPolyTests.lean: Added a public import of CompPolyTests.Fields.Mersenne31.Instances to the test file's import block. This makes the instances defined in that module (likely typeclass instances for the Mersenne31 field, such as Field, Fintype, or Ring instances) available to all downstream consumers of this test file, which may be necessary for subsequent tests or proofs that rely on those instances being in the ambient context.
• tests/CompPolyTests/Fields/Mersenne31/Fast.lean: Added two #guard statements to the Mersenne31.Fast namespace that test the ringEquiv function preserves addition and multiplication: ringEquiv ((123 : Field) + 456) = ((123 : Mersenne31.Field) + 456) and ringEquiv ((123 : Field) * 456) = ((123 : Mersenne31.Field) * 456). These guard against regressions in the ring isomorphism between the two field representations.
• tests/CompPolyTests/Fields/Mersenne31/Instances.lean: This new file tests/CompPolyTests/Fields/Mersenne31/Instances.lean adds regression-check examples that verify the Mersenne31 and Mersenne31.Fast field types satisfy key typeclass instances: Fact (Nat.Prime fieldSize), Field, and NonBinaryField. It also includes an explicit proof that (2 : Mersenne31.Field) ≠ 0 using NonBinaryField.char_neq_2. No sorry, admit, or unimplemented proofs are present; all examples are closed by inferInstance or a single application of exact. The file ensures these instances remain available and correctly inferred as the project evolves.

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.